$\in$$x$:$T$. $P$($x$) $\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$Case ${\it xm}$(\{$y$:$T$$\mid$ $P$($y$) \}) of inl($z$) $\Rightarrow$ $z$ ; inr($w$) $\Rightarrow$ "???"